/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓␈↓ αTSeveral␈αpeople␈αhave␈αcommented␈αthat␈αthe␈αminimization␈αschema␈αseems␈αto␈αbe␈αcreeping␈αsecond
␈↓ α∧␈↓order␈αlogic.␈α
 Indeed␈αit␈α
steps␈αbeyond␈α
the␈αaxiom␈α
schema␈αof␈α
induction␈αof␈α
Peano␈αarithmetic␈α
in␈αthat␈α
we
␈↓ α∧␈↓have␈α∞a␈α∞schema␈α∞for␈α∂each␈α∞function␈α∞rather␈α∞than␈α∞a␈α∂single␈α∞schema.␈α∞ However,␈α∞our␈α∞method␈α∂of␈α∞proof
␈↓ α∧␈↓using␈α∞it␈α∞as␈α
implemented␈α∞in␈α∞Richard␈α∞Weyhrauch's␈α
proof-checker␈α∞and␈α∞interactive␈α∞theorem␈α
prover
␈↓ α∧␈↓FOL␈α
is␈α
still␈α
basically␈αfirst␈α
order.␈α
 It␈α
has␈α
the␈αweakness␈α
of␈α
all␈α
first␈αorder␈α
systems␈α
in␈α
that␈α
it␈αdoesn't
␈↓ α∧␈↓permit␈α∂proving␈α∂statements␈α∂that␈α∂quantify␈α∂over␈α∂functions.␈α∂ It␈α∂has␈α∂the␈α∂strength␈α∂that␈α∂the␈α∂G␈↓
:␈↓odelian
␈↓ α∧␈↓incompleteness␈αis␈αin␈αthe␈αaxiomatization␈αrather␈αthan␈αin␈αthe␈αlogic.␈α Moreover,␈αR.␈αS.␈αCartwright␈αhas
␈↓ α∧␈↓recently␈α
shown␈α
that␈αany␈α
sentence␈α
containing␈αa␈α
function␈α
characterized␈αby␈α
a␈α
functional␈αequation␈α
and
␈↓ α∧␈↓minimization␈α∩schema␈α∩can␈α∩be␈α∩proved␈α∩in␈α∩first␈α∪order␈α∩logic␈α∩to␈α∩be␈α∩equivalent␈α∩to␈α∩a␈α∪sentence␈α∩not
␈↓ α∧␈↓involving␈α
the␈α
function␈αbut␈α
only␈α
␈↓↓car,␈↓␈α
␈↓↓cdr,␈↓␈α␈↓↓cons,␈↓␈α
␈↓↓atom␈↓␈α
and␈α
␈↓↓occur.␈↓␈αThus␈α
the␈α
incompleteness␈α
is␈αin␈α
the
␈↓ α∧␈↓axiomatization␈α
of␈α
the␈α
domain␈α
rather␈α
than␈αin␈α
the␈α
logic.␈α
 I␈α
think␈α
this␈αis␈α
the␈α
essence␈α
of␈α
the␈α
issue␈αas␈α
to
␈↓ α∧␈↓whether the logic is first or second order.

␈↓ α∧␈↓␈↓ αTAlthough␈αwe␈αdon't␈αhave␈αmuch␈αpractical␈αexperience␈αwith␈αthe␈αminimization␈αschema,␈αwe␈αhave
␈↓ α∧␈↓used␈α∪it␈α∪to␈α∪prove␈α∪partial␈α∪correctness␈α∪and␈α∪to␈α∪prove␈α∪that␈α∪a␈α∪function␈α∪is␈α∪not␈α∪total.␈α∀ Mostly␈α∪the
␈↓ α∧␈↓comparison␈α∞functions␈α∞have␈α
not␈α∞been␈α∞recursive,␈α∞but␈α
it␈α∞has␈α∞also␈α∞been␈α
used␈α∞to␈α∞get␈α∞results␈α
formerly
␈↓ α∧␈↓proved with my now retired method of recursion induction.  On the whole, it looks convenient.